Nuprl Lemma : ccsucc_wf
11,40
postcript
pdf
id
:Id,
num
:
. ccsucc(
id
;
num
)
chain_config()
latex
Definitions
ccsucc(
id
;
num
)
,
chain_config()
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
unit
wf
,
Id
wf
,
nat
wf
origin
id:Id, num:
. ccsucc(id;num) 
chain_config() id:Id, num:. ccsucc(id;num) chain_config() Tx:A. B(x)